Inference at * 1 2 0 
Iof proof for Lemma l before antisymmetry:



1. T : Type
2. l : T List
3. x : T
4. y : T
5. no_repeats(T;l)
6. [x; y]  l
7. [y; x]  l
8. [x; x]  l
  False 

latex

 by PERMUTE{1:n, 1:n, 2:n, 3:n} 

latex

 1: .....wf..... NILNIL

 1: 5. x, y:T. [x; y]  l  ((x = y))
 1: 6. [x; y]  l
 1: 7. [y; x]  l
 1: 8. [x; x]  l
 1:   x  T
 2: .....antecedent..... NILNIL

 2: 5. x, y:T. [x; y]  l  ((x = y))
 2: 6. [x; y]  l
 2: 7. [y; x]  l
 2: 8. [x; x]  l
 2:   [x; x]  l
 3: 

 3: 5. x, y:T. [x; y]  l  ((x = y))
 3: 6. [x; y]  l
 3: 7. [y; x]  l
 3: 8. [x; x]  l
 3: 9. (x = x)
 3:   False
 .

Definitions	x:A  B(x), P  Q, f(a), x:AB(x), s = t, A, False, [], [car / cdr], L1  L2, no_repeats(T;l), type List, Type, P & Q, P  Q, x before y  l, x:A. B(x), P  Q, t  T
Lemmas	no repeats iff